ea,eb:( List), x:(?), f,g:(). combine-halt-info(ea; eb; f; g; x)  (?) 

latex

Definitions	t  T, , x:A. B(x), Unit, , A  B, P  Q, False, A, ff, nat-deq, deq-member(eq; x; L), band(p; q), if b then t else f fi , tt, isl(x), merge(as; bs), x,y. t(x;y), list_accum(x,a.f(x;a); y; l), combine-halt-info(ea; eb; f; g; x)
Lemmas	list accum wf, merge wf, isl wf, btrue wf, ifthenelse wf, band wf, deq-member wf, nat-deq wf, bfalse wf, le wf, bool wf, unit wf, nat wf